<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>

<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.09">
<LINK rel="stylesheet" type="text/css" href="Reference-Manual.css">
<TITLE>Index of Error Messages</TITLE>
</HEAD>
<BODY >
<A HREF="command-index.html"><IMG SRC="previous_motif.gif" ALT="Previous"></A>
<A HREF="toc.html"><IMG SRC="contents_motif.gif" ALT="Up"></A>
<HR>
<H1 CLASS="chapter">Index of Error Messages</H1><P></P><TABLE CELLSPACING=6 CELLPADDING=0><TR><TD VALIGN=top ALIGN=left><UL CLASS="indexenv"><LI CLASS="li-indexenv">
<I><FONT COLOR=maroon>ident</FONT></I><SUB>2</SUB> not found, <A HREF="Reference-Manual010.html#@error61">1</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>ident</FONT></I><SUB><I>i</I></SUB> not found, <A HREF="Reference-Manual010.html#@error58">1</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>ident</FONT></I> already exists, <A HREF="Reference-Manual003.html#@error0">1</A>, <A HREF="Reference-Manual003.html#@error1">1</A>, <A HREF="Reference-Manual003.html#@error2">1</A>, <A HREF="Reference-Manual003.html#@error4">1</A>, <A HREF="Reference-Manual003.html#@error8">1</A>, <A HREF="Reference-Manual024.html#@error143">1</A>
</LI><LI CLASS="li-indexenv"><I><FONT COLOR=maroon>ident</FONT></I> not found, <A HREF="Reference-Manual010.html#@error55">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">A record cannot be recursive, <A HREF="Reference-Manual004.html#@error9">1</A>
</LI><LI CLASS="li-indexenv">Argument of match does not evaluate to a term, <A HREF="Reference-Manual011.html#@error119">2</A>
</LI><LI CLASS="li-indexenv">Attempt to save an incomplete proof, <A HREF="Reference-Manual009.html#@error40">1</A>
</LI><LI CLASS="li-indexenv">already exists, <A HREF="Reference-Manual009.html#@error42">2</A>
</LI><LI CLASS="li-indexenv">arguments of ring_simplify do not have all the same type, <A HREF="Reference-Manual025.html#@error146">2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Bad magic number, <A HREF="Reference-Manual008.html#@error33">3</A>
</LI><LI CLASS="li-indexenv">Bound head variable, <A HREF="Reference-Manual010.html#@error108">1</A>, <A HREF="Reference-Manual010.html#@error110">1</A>
</LI><LI CLASS="li-indexenv">bad lemma for decidability of equality, <A HREF="Reference-Manual025.html#@error150">2</A>
</LI><LI CLASS="li-indexenv">bad ring structure, <A HREF="Reference-Manual025.html#@error149">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Can't find file <I><FONT COLOR=maroon>ident</FONT></I> on loadpath, <A HREF="Reference-Manual008.html#@error30">1</A>
</LI><LI CLASS="li-indexenv">Can't find module toto on loadpath, <A HREF="Reference-Manual008.html#@error32">2</A>
</LI><LI CLASS="li-indexenv">Cannot build functional inversion principle, <A HREF="Reference-Manual004.html#@error15">6</A>
</LI><LI CLASS="li-indexenv">Cannot define graph for <I><FONT COLOR=maroon>ident</FONT></I>&#X2026;, <A HREF="Reference-Manual004.html#@error13">4</A>
</LI><LI CLASS="li-indexenv">Cannot define principle(s) for <I><FONT COLOR=maroon>ident</FONT></I>&#X2026;, <A HREF="Reference-Manual004.html#@error14">5</A>
</LI><LI CLASS="li-indexenv">Cannot find induction information on <I><FONT COLOR=maroon>qualid</FONT></I>, <A HREF="Reference-Manual010.html#@error90">1</A>
</LI><LI CLASS="li-indexenv">Cannot find inversion information for hypothesis <I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual010.html#@error103">2</A>
</LI><LI CLASS="li-indexenv">Cannot find the source class of <I><FONT COLOR=maroon>qualid</FONT></I>, <A HREF="Reference-Manual021.html#@error130">6</A>
</LI><LI CLASS="li-indexenv">Cannot infer a term for this placeholder, <A HREF="Reference-Manual004.html#@error22">1</A>, <A HREF="Reference-Manual010.html#@error53">3</A>
</LI><LI CLASS="li-indexenv">Cannot load <I><FONT COLOR=maroon>ident</FONT></I>: no physical path bound to <I><FONT COLOR=maroon>dirpath</FONT></I>, <A HREF="Reference-Manual008.html#@error31">1</A>
</LI><LI CLASS="li-indexenv">Cannot move <I><FONT COLOR=maroon>ident</FONT></I><SUB>1</SUB> after <I><FONT COLOR=maroon>ident</FONT></I><SUB>2</SUB>:
it depends on <I><FONT COLOR=maroon>ident</FONT></I><SUB>2</SUB>, <A HREF="Reference-Manual010.html#@error60">3</A>
</LI><LI CLASS="li-indexenv">Cannot move <I><FONT COLOR=maroon>ident</FONT></I><SUB>1</SUB> after <I><FONT COLOR=maroon>ident</FONT></I><SUB>2</SUB>:
it occurs in <I><FONT COLOR=maroon>ident</FONT></I><SUB>2</SUB>, <A HREF="Reference-Manual010.html#@error59">2</A>
</LI><LI CLASS="li-indexenv">Cannot recognize <I><FONT COLOR=maroon>class</FONT></I><SUB>1</SUB> as a source class of <I><FONT COLOR=maroon>qualid</FONT></I>, <A HREF="Reference-Manual021.html#@error131">7</A>
</LI><LI CLASS="li-indexenv">Cannot refine to conclusions with meta-variables, <A HREF="Reference-Manual010.html#@error87">2</A>
</LI><LI CLASS="li-indexenv">Cannot solve the goal, <A HREF="Reference-Manual011.html#@error116">9.2</A>
</LI><LI CLASS="li-indexenv">Cannot use mutual definition with well-founded
recursion or measure, <A HREF="Reference-Manual004.html#@error12">3</A>
</LI><LI CLASS="li-indexenv">cannot be used as a hint, <A HREF="Reference-Manual010.html#@error109">2</A>, <A HREF="Reference-Manual010.html#@error111">2</A>
</LI><LI CLASS="li-indexenv">cannot find a declared ring structure for equality
<TT>term</TT>, <A HREF="Reference-Manual025.html#@error148">4</A>
</LI><LI CLASS="li-indexenv">cannot find a declared ring structure over <TT>term</TT>, <A HREF="Reference-Manual025.html#@error147">3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Delta must be specified before, <A HREF="Reference-Manual010.html#@error80">1</A>
</LI><LI CLASS="li-indexenv">does not denote an evaluable constant, <A HREF="Reference-Manual010.html#@error82">1</A>
</LI><LI CLASS="li-indexenv">does not respect the inheritance uniform condition, <A HREF="Reference-Manual021.html#@error132">8</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Error: The term &#X201C;<I><FONT COLOR=maroon>term</FONT></I>&#X201D; has type <I><FONT COLOR=maroon>type</FONT></I> while it is expected to have type &#X201C;<I><FONT COLOR=maroon>type</FONT></I>&#X201D;, <A HREF="Reference-Manual003.html#@error3">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Failed to progress, <A HREF="Reference-Manual011.html#@error114">9.2</A>
</LI><LI CLASS="li-indexenv">File not found on loadpath : <I><FONT COLOR=maroon>string</FONT></I>, <A HREF="Reference-Manual008.html#@error34">1</A>
</LI><LI CLASS="li-indexenv">Found target class <I><FONT COLOR=maroon>class</FONT></I> instead of <I><FONT COLOR=maroon>class</FONT></I><SUB>2</SUB>, <A HREF="Reference-Manual021.html#@error133">9</A>
</LI><LI CLASS="li-indexenv">Funclass cannot be a source class, <A HREF="Reference-Manual021.html#@error127">3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Goal is solvable by congruence but some arguments are missing. Try congruence with &#X2026;, replacing metavariables by arbitrary terms., <A HREF="Reference-Manual010.html#@error107">3</A>
</LI><LI CLASS="li-indexenv">generated subgoal <I><FONT COLOR=maroon>term</FONT></I>' has metavariables in it, <A HREF="Reference-Manual010.html#@error73">2</A>
</LI><LI CLASS="li-indexenv">goal does not satisfy the expected preconditions, <A HREF="Reference-Manual010.html#@error101">2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Hypothesis <I><FONT COLOR=maroon>ident</FONT></I>must contain at least one Function, <A HREF="Reference-Manual010.html#@error102">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">I couldn't solve goal, <A HREF="Reference-Manual010.html#@error106">2</A>
</LI><LI CLASS="li-indexenv">I don't know how to handle dependent equality, <A HREF="Reference-Manual010.html#@error105">1</A>
</LI><LI CLASS="li-indexenv">Impossible to unify &#X2026; with .., <A HREF="Reference-Manual010.html#@error96">2</A>
</LI><LI CLASS="li-indexenv">Impossible to unify &#X2026; with &#X2026;, <A HREF="Reference-Manual010.html#@error72">1</A>, <A HREF="Reference-Manual010.html#@error89">10</A>
</LI><LI CLASS="li-indexenv">In environment &#X2026; the term: <I><FONT COLOR=maroon>term</FONT></I><SUB>2</SUB> does not have type
<I><FONT COLOR=maroon>term</FONT></I><SUB>1</SUB>, <A HREF="Reference-Manual024.html#@error144">1</A>
</LI><LI CLASS="li-indexenv">invalid argument, <A HREF="Reference-Manual010.html#@error52">1</A>
</LI><LI CLASS="li-indexenv">is
used in the hypothesis, <A HREF="Reference-Manual010.html#@error57">3</A>
</LI><LI CLASS="li-indexenv">is already a coercion, <A HREF="Reference-Manual021.html#@error126">2</A>
</LI><LI CLASS="li-indexenv">is already used, <A HREF="Reference-Manual010.html#@error62">2</A>, <A HREF="Reference-Manual010.html#@error64">2</A>
</LI><LI CLASS="li-indexenv">is not a function, <A HREF="Reference-Manual021.html#@error129">5</A>
</LI><LI CLASS="li-indexenv">is not a module, <A HREF="Reference-Manual004.html#@error21">1</A>
</LI><LI CLASS="li-indexenv">is not a projectable equality, <A HREF="Reference-Manual010.html#@error99">1</A>
</LI><LI CLASS="li-indexenv">is not an inductive type, <A HREF="Reference-Manual010.html#@error112">1</A>
</LI><LI CLASS="li-indexenv">is used in the
conclusion, <A HREF="Reference-Manual010.html#@error56">2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Loading of ML object file forbidden in a native Coq, <A HREF="Reference-Manual008.html#@error35">2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Module/section <I><FONT COLOR=maroon>module</FONT></I> not found, <A HREF="Reference-Manual008.html#@error28">2(a)</A>
</LI><LI CLASS="li-indexenv">must be a transparent constant, <A HREF="Reference-Manual021.html#@error134">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">No applicable tactic, <A HREF="Reference-Manual011.html#@error115">9.2</A>
</LI></UL></TD><TD VALIGN=top ALIGN=left><UL CLASS="indexenv"><LI CLASS="li-indexenv">No argument name <I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@error11">2</A>
</LI><LI CLASS="li-indexenv">No discriminable equalities, <A HREF="Reference-Manual010.html#@error98">2(a)</A>
</LI><LI CLASS="li-indexenv">No focused
proof, <A HREF="Reference-Manual009.html#@error38">7</A>
</LI><LI CLASS="li-indexenv">No focused proof, <A HREF="Reference-Manual009.html#@error50">1(b)</A>
</LI><LI CLASS="li-indexenv">No focused proof (No proof-editing in progress), <A HREF="Reference-Manual009.html#@error43">1</A>, <A HREF="Reference-Manual009.html#@error46">1</A>
</LI><LI CLASS="li-indexenv">No focused proof to restart, <A HREF="Reference-Manual009.html#@error48">1</A>
</LI><LI CLASS="li-indexenv">No matching clauses for match, <A HREF="Reference-Manual011.html#@error118">1</A>
</LI><LI CLASS="li-indexenv">No matching clauses for match goal, <A HREF="Reference-Manual011.html#@error120">9.2</A>
</LI><LI CLASS="li-indexenv">No product even after head-reduction, <A HREF="Reference-Manual010.html#@error63">1</A>, <A HREF="Reference-Manual010.html#@error68">6(a)</A>, <A HREF="Reference-Manual010.html#@error70">7(a)</A>
</LI><LI CLASS="li-indexenv">No proof-editing in progress, <A HREF="Reference-Manual009.html#@error44">1</A>
</LI><LI CLASS="li-indexenv">No such assumption, <A HREF="Reference-Manual010.html#@error54">1</A>, <A HREF="Reference-Manual010.html#@error79">1</A>
</LI><LI CLASS="li-indexenv">No such goal, <A HREF="Reference-Manual009.html#@error49">1(a)</A>
</LI><LI CLASS="li-indexenv">No such hypothesis, <A HREF="Reference-Manual010.html#@error69">6(b)</A>, <A HREF="Reference-Manual010.html#@error71">7(b)</A>, <A HREF="Reference-Manual010.html#@error83">1</A>
</LI><LI CLASS="li-indexenv">No such hypothesis in current goal, <A HREF="Reference-Manual010.html#@error66">4</A>, <A HREF="Reference-Manual010.html#@error67">5</A>
</LI><LI CLASS="li-indexenv">No such label <I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual004.html#@error17">1</A>
</LI><LI CLASS="li-indexenv">No such proof, <A HREF="Reference-Manual009.html#@error45">1</A>
</LI><LI CLASS="li-indexenv">Non exhaustive pattern-matching, <A HREF="Reference-Manual020.html#@error124">2</A>
</LI><LI CLASS="li-indexenv">Non strictly positive occurrence of <I><FONT COLOR=maroon>ident</FONT></I> in <I><FONT COLOR=maroon>type</FONT></I>, <A HREF="Reference-Manual003.html#@error5">1</A>
</LI><LI CLASS="li-indexenv">Not a discriminable equality, <A HREF="Reference-Manual010.html#@error97">1</A>
</LI><LI CLASS="li-indexenv">Not a proposition or a type, <A HREF="Reference-Manual010.html#@error75">1</A>
</LI><LI CLASS="li-indexenv">Not a valid (semi)ring theory, <A HREF="Reference-Manual025.html#@error152">1</A>
</LI><LI CLASS="li-indexenv">Not an equation, <A HREF="Reference-Manual010.html#@error100">2</A>
</LI><LI CLASS="li-indexenv">Not an exact proof, <A HREF="Reference-Manual010.html#@error51">1</A>
</LI><LI CLASS="li-indexenv">Not an inductive product, <A HREF="Reference-Manual010.html#@error84">1</A>, <A HREF="Reference-Manual010.html#@error86">1</A>
</LI><LI CLASS="li-indexenv">Not convertible, <A HREF="Reference-Manual010.html#@error78">1</A>
</LI><LI CLASS="li-indexenv">Not enough constructors, <A HREF="Reference-Manual010.html#@error85">2</A>
</LI><LI CLASS="li-indexenv">Not reducible, <A HREF="Reference-Manual010.html#@error81">1</A>
</LI><LI CLASS="li-indexenv">Not the right number of dependent arguments, <A HREF="Reference-Manual010.html#@error88">7</A>
</LI><LI CLASS="li-indexenv">Not the right number of induction arguments, <A HREF="Reference-Manual010.html#@error91">2</A>
</LI><LI CLASS="li-indexenv">Not the right number of missing arguments, <A HREF="Reference-Manual010.html#@error74">1</A>
</LI><LI CLASS="li-indexenv">name <I><FONT COLOR=maroon>ident</FONT></I> is already used, <A HREF="Reference-Manual010.html#@error65">2</A>
</LI><LI CLASS="li-indexenv">no such entry, <A HREF="Reference-Manual008.html#@error36">1</A>
</LI><LI CLASS="li-indexenv">not a context variable, <A HREF="Reference-Manual011.html#@error121">9.2</A>
</LI><LI CLASS="li-indexenv">not a defined object, <A HREF="Reference-Manual008.html#@error24">1</A>
</LI><LI CLASS="li-indexenv">not a valid ring equation, <A HREF="Reference-Manual025.html#@error145">1</A>
</LI><LI CLASS="li-indexenv">not declared, <A HREF="Reference-Manual010.html#@error113">2</A>, <A HREF="Reference-Manual021.html#@error125">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">omega can't solve this system, <A HREF="Reference-Manual022.html#@error135">1</A>
</LI><LI CLASS="li-indexenv">omega: Can't solve a goal with equality on <I><FONT COLOR=maroon>type</FONT></I>, <A HREF="Reference-Manual022.html#@error142">8</A>
</LI><LI CLASS="li-indexenv">omega: Can't solve a goal with non-linear products, <A HREF="Reference-Manual022.html#@error141">7</A>
</LI><LI CLASS="li-indexenv">omega: Can't solve a goal with proposition variables, <A HREF="Reference-Manual022.html#@error139">5</A>
</LI><LI CLASS="li-indexenv">omega: Not a quantifier-free goal, <A HREF="Reference-Manual022.html#@error136">2</A>
</LI><LI CLASS="li-indexenv">omega: Unrecognized atomic proposition: <I><FONT COLOR=maroon>prop</FONT></I>, <A HREF="Reference-Manual022.html#@error138">4</A>
</LI><LI CLASS="li-indexenv">omega: Unrecognized predicate or connective: <I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual022.html#@error137">3</A>
</LI><LI CLASS="li-indexenv">omega: Unrecognized proposition, <A HREF="Reference-Manual022.html#@error140">6</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Proof is not complete, <A HREF="Reference-Manual011.html#@error122">9.2</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">quote: not a simple fixpoint, <A HREF="Reference-Manual010.html#@error104">1</A>, <A HREF="Reference-Manual012.html#@error123">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Reached begin of command history, <A HREF="Reference-Manual008.html#@error37">1</A>
</LI><LI CLASS="li-indexenv">ring <I>operation</I> should be declared as a morphism, <A HREF="Reference-Manual025.html#@error151">3</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Signature components for label <I><FONT COLOR=maroon>ident</FONT></I> do not match, <A HREF="Reference-Manual004.html#@error18">2</A>
</LI><LI CLASS="li-indexenv">Sortclass cannot be a source class, <A HREF="Reference-Manual021.html#@error128">4</A>
</LI><LI CLASS="li-indexenv">Statement without assumptions, <A HREF="Reference-Manual010.html#@error76">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Tactic Failure <I>message</I> (level <I>n</I>), <A HREF="Reference-Manual011.html#@error117">9.2</A>
</LI><LI CLASS="li-indexenv">Tactic generated a subgoal identical to the original goal, <A HREF="Reference-Manual010.html#@error93">2</A>
</LI><LI CLASS="li-indexenv">The <I><FONT COLOR=maroon>num</FONT></I>th argument of <I><FONT COLOR=maroon>ident</FONT></I> must be <I><FONT COLOR=maroon>ident</FONT></I>' in
<I><FONT COLOR=maroon>type</FONT></I>, <A HREF="Reference-Manual003.html#@error7">1</A>
</LI><LI CLASS="li-indexenv">The conclusion is not a substitutive equation, <A HREF="Reference-Manual010.html#@error95">1</A>
</LI><LI CLASS="li-indexenv">The conclusion of <I><FONT COLOR=maroon>type</FONT></I> is not valid; it must be
built from <I><FONT COLOR=maroon>ident</FONT></I>, <A HREF="Reference-Manual003.html#@error6">2</A>
</LI><LI CLASS="li-indexenv">The recursive argument must be specified, <A HREF="Reference-Manual004.html#@error10">1</A>
</LI><LI CLASS="li-indexenv">The reference <I><FONT COLOR=maroon>qualid</FONT></I> was not found in the current
environment, <A HREF="Reference-Manual008.html#@error25">1</A>, <A HREF="Reference-Manual008.html#@error26">1</A>, <A HREF="Reference-Manual008.html#@error27">1</A>, <A HREF="Reference-Manual008.html#@error29">1</A>
</LI><LI CLASS="li-indexenv">The term provided does not end with an equation, <A HREF="Reference-Manual010.html#@error92">1</A>
</LI><LI CLASS="li-indexenv">This is not the last opened module, <A HREF="Reference-Manual004.html#@error19">3</A>
</LI><LI CLASS="li-indexenv">This is not the last opened module type, <A HREF="Reference-Manual004.html#@error20">1</A>
</LI><LI CLASS="li-indexenv">This is not the last opened section, <A HREF="Reference-Manual004.html#@error16">1</A>
</LI><LI CLASS="li-indexenv">terms do not have convertible types, <A HREF="Reference-Manual010.html#@error94">1</A>
</LI><LI CLASS="li-indexenv">the term <I><FONT COLOR=maroon>form</FONT></I> has type &#X2026; which should be Set,
Prop or Type, <A HREF="Reference-Manual009.html#@error39">1</A>, <A HREF="Reference-Manual009.html#@error41">1</A>
<BR>
<BR>
</LI><LI CLASS="li-indexenv">Unable to apply, <A HREF="Reference-Manual010.html#@error77">2</A>
</LI><LI CLASS="li-indexenv">Undo stack would be exhausted, <A HREF="Reference-Manual009.html#@error47">2</A>
</LI><LI CLASS="li-indexenv">Universe
inconsistency, <A HREF="Reference-Manual006.html#@error23">4.1.1</A>
</LI></UL></TD></TR>
</TABLE><HR>
<A HREF="command-index.html"><IMG SRC="previous_motif.gif" ALT="Previous"></A>
<A HREF="toc.html"><IMG SRC="contents_motif.gif" ALT="Up"></A>
</BODY>
</HTML>
